#include "converter.h"

char* ganti,hasil;
int p1;

void copy_tree(address X, address Y) {
    (*Y) = (*X);
    if (Left(Y) != NULL) {
        Left(Y) = malloc(sizeof(node));
        copy_tree(Left(X), Left(Y));
    }
    if (Right(Y) != NULL) {
        Right(Y) = malloc(sizeof(node));
        copy_tree(Right(X), Right(Y));
    }
}

void implication(address X) {
    if (Operator(X) == '>') {
        //p -> q,  change into -p | q
        Operator(X) = '|';
        address nega = malloc(sizeof(node));
        Operator(nega) = '-';
        Left(nega) = Left(X);
        Left(X) = nega;
        flag = true;
    } else if (Operator(X) == '<') {
        //p <- q,  change into p | -q
        Operator(X) = '|';
        address nega = malloc(sizeof(node));
        Operator(nega) = '-';
        Left(nega) = Right(X);
        Right(X) = nega;
        flag = true;
    } else if (Operator(X) == '=') {
        //p <-> q, change into (p -> q) & (p <- q)
        //that way, hopefully we will have less work for
        //the rest of the conversion
        flag = true;
        Operator(X) = '&';
        address kiri = malloc(sizeof(node));
        address kanan = malloc(sizeof(node));
        Left(kiri) = Left(X);
        Right(kiri) = Right(X);
        Left(X) = kiri;
        Right(X) = kanan;
        Operator(kiri) = '>';
        copy_tree(kiri,kanan);
        Operator(kanan) = '<';
    }
    
    if ((!flag)&&(Left(X) != NULL)) {
		implication(Left(X));
	}
    if ((!flag)&&(Right(X) != NULL)) {
		implication(Right(X));
	}
}

void negation(address X, address* parent) {
    //pada tahap ini, tidak ada operasi >, <, dan =
    //jadi kasus-kasus tersebut tidak perlu dihandle.
    //pada awalnya, semua term diberikan kode f.
    //baru setelah tahap negation in selesai, ada kode n.

    //kasus n tidak diatasi karena : 
    //1. Ini adalah tree, dan proses dilakukan dari root menuju leaf.
    //2. Term hanya mungkin terletak pada leaf.
    //3. Operasi negation bekerja dengan cara mendorong operator negasi sejauh-jauhnya
    //   ke leaf sambil melakukan operasi pengubahan yang diperlukan.
    //4. Semua leaf maksimal menerima operasi pengubahan satu kali.
    //5. Maka, pasti jika ada pengubahan operator leaf, itu dari f ke n.
    
    if (Operator(X) == '-') {
        address temp = Left(X);
        if ((Operator(temp) != 'f') && (Operator(temp) != 'n')) flag = true;
        if (Operator(temp) == '-') {
            //double negation, just erase both of them
            *parent = Left(temp);
            free(temp);
        } else if (Operator(temp) == '&') {
            //-(p & q), change into -p | -q
            *parent = temp;            
            Operator(temp) = '|';
            
            address kiri = malloc(sizeof(node));
            address kanan = malloc(sizeof(node));
            Operator(kiri) = Operator(kanan) = '-';
            Right(kiri) = Right(kanan) = NULL;
            Left(kiri) = Left(temp);
            Left(temp) = kiri;
            Left(kanan) = Right(temp);
            Right(temp) = kanan;
        } else if (Operator(temp) == '|') {
            //-(p | q), change into -p & -q
            *parent = temp;            
            Operator(temp) = '&';
            
            address kiri = malloc(sizeof(node));
            address kanan = malloc(sizeof(node));
            Operator(kiri) = Operator(kanan) = '-';
            Right(kiri) = Right(kanan) = NULL;
            Left(kiri) = Left(temp);
            Left(temp) = kiri;
            Left(kanan) = Right(temp);
            Right(temp) = kanan;        
        } else if (Operator(temp) == 'a') {
            //-(all x(p)), ganti jadi exists x(-(p))
            *parent = temp;
            Operator(temp) = 'e';
            
            address kiri = malloc(sizeof(node));
            Operator(kiri) = '-';
            Right(kiri) = NULL;
            Left(kiri) = Left(temp);
            Left(temp) = kiri;
        } else if (Operator(temp) == 'e') {
            //-(exists x(p)), ganti jadi all x(-(p))
            *parent = temp;
            Operator(temp) = 'a';
            
            address kiri = malloc(sizeof(node));
            Operator(kiri) = '-';
            Right(kiri) = NULL;
            Left(kiri) = Left(temp);
            Left(temp) = kiri;        
        } else if (Operator(temp) == 'f') {
            Operator(temp) = 'n';
            *parent = temp;
        }
    }
    
    if ((!flag)&&(Left(X) != NULL)) negation(Left(X), &Left(X));
    if ((!flag)&&(Right(X) != NULL)) negation(Right(X), &Right(X));
    if (Operator(X) == '-') free(X);
}

void var_search(address X, char* kata) {
    if (!ada && ((Operator(X) == 'a') || (Operator(X) == 'e'))) {
        if (!strcmp(kata, Isi(X))) {
            ada = true;
            p1 = strlen(kata);
            variable[tvar] = malloc(p1 + 5);
            strcpy(variable[tvar], kata);
            int i;
            //printf("%s\n",kata);
            
            do {
                flag = false;
                ++changeid;
                int sem = changeid;
                for (i = p1;sem > 0;++i) {
                    variable[tvar][i] = (sem % 10) + 48;
                    sem /= 10;
                }
                variable[tvar][i] = 0;
                
                for (i=0;i<tvar && !flag;++i) {
                    flag = (strcmp(variable[i],variable[tvar]) == 0);
                }
            } while (flag);
            
            p1 = strlen(variable[tvar]);
            ++tvar;
            var_search(Left(X), kata);
            free(Isi(X));
            Isi(X) = malloc(p1+1);
            strcpy(Isi(X), variable[tvar-1]);
            
            flag = true;
            ada = false;
        }
    } else if (ada) {
        if (Isi(X) != NULL) {
            char temp[p1*MaxLn];
            memset(temp,0,sizeof(temp));
            int panjang = strlen(Isi(X));
            int total = 0,i,j,last = 0;    
            
            for (i=0;i<=panjang;++i) {
                if (!isalphanum(Isi(X)[i])) {
                    if (!strcmp(temp + last,kata)) {
                        while (total > last) {
                            temp[--total] = 0;
                        }
                        
                        for (j=0;j<p1;++j) {
                            temp[total++] = variable[tvar-1][j];
                        }
                    }
                    last = total+1;
                }
                temp[total++] = Isi(X)[i];
            }
            
            if (strcmp(temp, Isi(X))) {
                free(Isi(X));
                Isi(X) = malloc(total+1);
                strcpy(Isi(X),temp);
            }
        }
    }
    
    if ((!flag)&&(Left(X) != NULL)) var_search(Left(X), kata);
    if ((!flag)&&(Right(X) != NULL)) var_search(Right(X), kata);
}

void standardize(address X) {
    if ((Operator(X) == 'a')||(Operator(X) == 'e')) {
        var_search(Left(X), Isi(X));
    }
    
    if ((!flag)&&(Left(X) != NULL)) standardize(Left(X));
    if ((!flag)&&(Right(X)) != NULL) standardize(Right(X));
}

void switch_var(address X, char* dari, char* ke) {
    if ((Operator(X) == 'f')||(Operator(X) == 'n')) {
        char temp[MaxCol*2];
        memset(temp,0,sizeof(temp));
        int panjang = strlen(Isi(X));
        int total = 0,i,j,last = 0;    
        
        for (i=0;i<=panjang;++i) {
            if (!isalphanum(Isi(X)[i])) {
                if (!strcmp(temp + last,dari)) {
                    while (total > last) {
                        temp[--total] = 0;
                    }
                    
                    j=0;
                    while (ke[j]) {
                        temp[total++] = ke[j];
                        ++j;
                    }
                }
                last = total+1;
            }
            temp[total++] = Isi(X)[i];
        }
        
        if (strcmp(temp, Isi(X))) {
            free(Isi(X));
            Isi(X) = malloc(total+1);
            strcpy(Isi(X),temp);
        }       
    } else {
        if (Left(X) != NULL) switch_var(Left(X),dari,ke);
        if (Right(X) != NULL) switch_var(Right(X),dari,ke);
    }
}

void existential(address* X) {
    if (Operator(*X) == 'e') {
        //Buang quantifier existensial, ganti ama fungsi
        //yang masukannya semua variable universal yang 
        //membungkus quantifier existensial tersebut.
        address z = *X;
        *X = Left(*X);
        ganti = Isi(z);
        free(z);
        char* baru;
        
        if (tact) {
            ++freef;
            int sem =freef,bagi = 1;
            int i,j,panjang = 9+tact;
            while (sem) {
                ++panjang;
                sem /= 10;
                bagi *= 10;
            }
            
            for (i=0;i<tact;++i) panjang += strlen(aktif[i]);
            baru = malloc(panjang);
            strcpy(baru,"fskolem");
            int pos = 7;
            sem =freef;
            bagi /= 10;
            
            while (bagi) {
                baru[pos++] = 48+sem / bagi;
                sem %= bagi;
                bagi /= 10;
            }
            
            baru[pos++] = '(';
            for (i=0;i<tact;++i) {
                if (i) baru[pos++] = ',';
                strcpy(baru+pos,aktif[i]);
                while (baru[pos]) ++pos;
            }
            
            baru[pos++] = ')';
            baru[pos++] = 0;
        } else {
            ++freec;
            int sem =freec,bagi = 1;
            int i,j,panjang = 6;
            while (sem) {
                ++panjang;
                sem /= 10;
                bagi *= 10;
            }        
        
            baru = malloc(panjang);
            strcpy(baru, "const");
            int pos = 5;
            sem = freec;
            bagi /= 10;
            while (bagi) {
                baru[pos++] = 48+sem / bagi;
                sem %= bagi;
                bagi /= 10;
            }
            baru[pos++] = 0;
        }
        
        switch_var(*X,ganti,baru);
        free(ganti);
        flag = true;
    } else if (Operator(*X) == 'a') {
        //tambahin ke dalam aktif
        aktif[tact] = malloc(strlen(Isi(*X)) + 1);
        strcpy(aktif[tact], Isi(*X));
        ++tact;
    }
    
    if ((!flag)&&(Left(*X) != NULL)) existential(&Left(*X));
    if ((!flag)&&(Right(*X)) != NULL) existential(&Right(*X));
    
    if (Operator(*X) == 'a') {
        //Jangan lupa, keluarin dulu dari aktif
        --tact;
        free(aktif[tact]);
    }
}

void all_out(address *X){
	if(Operator(*X) == 'a'){
		address z = *X;
		*X = Left(*X);
        free(Isi(z));
		free(z);
        flag = true;
		//all_out(X);
	} else {
		if ((!flag)&&(Left(*X)!= NULL)) all_out(&Left(*X));
		if ((!flag)&&(Right(*X)!= NULL)) all_out(&Right(*X));
	}
}

void distribution(address X) {
    address z,z0,z1,z2,tmp;
    if (Operator(X) == '|' && Operator(Left(X)) == '&') {
        //a & b | c, change into a | c & b | c

        z = malloc(sizeof(node));
        copy_tree(Right(X),z);
        z0 = Left(Left(X));
        z1 = Right(Left(X));
        z2 = Left(X);
        Operator(X) = '&';
        Operator(z2) = '|';
        Right(z2) = z;
        tmp = malloc(sizeof(node));
        Right(tmp) = Right(X);
        Right(X) = tmp;
        Operator(tmp) = '|';
        Left(tmp) = z1;
        flag = true;
    } else if (Operator(X) == '|' && Operator(Right(X)) == '&') {
        //a | b & c, change into a | b & a | c
        //well, in this code it is changed into a | c & b | a
        //which is equivalent to the first substitution written.
        
        z = malloc(sizeof(node));
        copy_tree(Left(X),z);
        z0 = Left(Right(X));
        z1 = Right(Right(X));
        z2 = Right(X);
        Operator(X) = '&';
        Operator(z2) = '|';
        Right(z2) = z;
        tmp = malloc(sizeof(node));
        Left(tmp) = Left(X);
        Left(X) = tmp;
        Operator(tmp) = '|';
        Right(tmp) = z1;
        flag = true;
    }
    
    if ((!flag)&&(Operator(X) == '&' || Operator(X) == '|')) {
        distribution(Left(X));
        distribution(Right(X));
    }
}

int ok;

void clausalform(address X) {
	if (Operator(X) == '&') {
		clausalform(Left(X));
        print_clause(BBB,0,ok);
		BBB++;
        member[BBB] = 0;
		clausalform(Right(X));
	} else if (Operator(X) == '|') {
		clausalform(Left(X));
		clausalform(Right(X));
	} else if (Operator(X) == 'n') {
        clauses[BBB][member[BBB]] = malloc(strlen(Isi(X)) + 1);
		strcpy(clauses[BBB][member[BBB]],Isi(X));
        positif[BBB][member[BBB]] = false;
        ++member[BBB];
	} else {
        clauses[BBB][member[BBB]] = malloc(strlen(Isi(X)) + 1);    
		strcpy(clauses[BBB][member[BBB]],Isi(X));
        positif[BBB][member[BBB]] = true;
        ++member[BBB];
	}
}

void convert() {
    int i;
    BBB = -1;
    for (i=1;i<=tpremis;++i) {
        printf("\nPremis #%d\n",i);
        print_tree(premis[i]);
        printf("\n");
        changeid = 0;
        
        printf("\n");
        do {
            printf("I : ");
            print_tree(premis[i]);
            printf("\n");  
            flag = false;
            implication(premis[i]);
        } while (flag);
        
        printf("\n");
        do {
            printf("N : ");
            print_tree(premis[i]);
            printf("\n");  
            flag = false;
            negation(premis[i], &premis[i]);          
        } while (flag);
        if (!prop) {
			printf("\n");
			do {
				printf("S : ");
				print_tree(premis[i]);
				printf("\n");  
				flag = ada = false;
				standardize(premis[i]);          
			} while (flag);      
			
			tact = 0;
			printf("\n");
			do {
				printf("E : ");
				print_tree(premis[i]);
				printf("\n");  
				flag = ada = false;
				existential(&premis[i]);          
			} while (flag);

			printf("\n");
			do {
				printf("A : ");
				print_tree(premis[i]);
				printf("\n");  
				flag = ada = false;
				all_out(&premis[i]);          
			} while (flag);
        }
        printf("\n");
        do {
            printf("D : ");
            print_tree(premis[i]);
            printf("\n");  
            flag = ada = false;
            distribution(premis[i]);          
        } while (flag);
        
        ++BBB;
        member[BBB] = 0;
        ok = i;
        clausalform(premis[i]);
        print_clause(BBB,0,i);
    }    
}

void convert_goal(int i) {
    printf("\nNegated Goal #%d\n",i);
    print_tree(ngoal[i]);
    printf("\n");
    changeid = 0;
    
    printf("\n");
    do {
        printf("I : ");
        print_tree(ngoal[i]);
        printf("\n");  
        flag = false;
        implication(ngoal[i]);
    } while (flag);
    
    printf("\n");
    do {
        printf("N : ");
        print_tree(ngoal[i]);
        printf("\n");  
        flag = false;
        negation(ngoal[i], &ngoal[i]);          
    } while (flag);
    
    printf("\n");
    do {
        printf("S : ");
        print_tree(ngoal[i]);
        printf("\n");  
        flag = ada = false;
        standardize(ngoal[i]);          
    } while (flag);      
    
    tact = 0;
    printf("\n");
    do {
        printf("E : ");
        print_tree(ngoal[i]);
        printf("\n");  
        flag = ada = false;
        existential(&ngoal[i]);          
    } while (flag);

    printf("\n");
    do {
        printf("A : ");
        print_tree(ngoal[i]);
        printf("\n");  
        flag = ada = false;
        all_out(&ngoal[i]);          
    } while (flag);
    
    printf("\n");
    do {
        printf("D : ");
        print_tree(ngoal[i]);
        printf("\n");  
        flag = ada = false;
        distribution(ngoal[i]);          
    } while (flag);
    
    ++BBB;
    member[BBB] = 0;
    clausalform(ngoal[i]);
    print_clause(BBB,1,i);
}
